Practical EMV Relay Protection

Andreea-Ina Radu, Tom Chothia, Christopher J.P. Newton, Ioana Boureanu and Liqun Chen

This work will be published at the 2022 IEEE Symposium on Security and Privacy

Download paper

Tamarin Models

Below is a brief summary of the formal models used in our paper, done using the Tamarin Prover.

Mobile Visa Model – Formal model for Visa transactions done via payment apps, in normal as well as transport mode (both Apple Pay, Samsung Pay are modelled).

Mobile Mastercard Model – Formal model for Mastercard transactions done via payment apps, in normal as well as transport mode (both Apple Pay, Samsung Pay are modelled).

Modified Basin Visa Model – An updated model for Visa transactions done via a (plastic) card, with more details around the [IAD] and its checks; it proves that checking the format of the IAD for Visa cards would in fact detect a previous contactless limit bypass attack proposed in The EMV Standard: Break, Fix, Verify.

L1RP Model – Formal model proving the security of our new proposed protocol, L1RP.